Forward Kani arguments to AutoHarness list commands - #674
wodex1nhaoIeng wants to merge 2 commits into
Conversation
|
Verified locally on origin/main base — after checking scripts/run-kani.sh in full, command_args is populated consistently with the rest of the script (command_args=("$@"), already forwarded via "${command_args[@]}" in several other invocation paths), so this fix follows the existing pattern rather than introducing something new. Ran --run list --with-autoharness --kani-args --include-pattern "" on this branch and confirmed the filter is actually reaching Kani (functions not matching the pattern come back tagged Did not match provided filters, which only appears once Kani receives the flag) — so the forwarding works end to end. |
|
Looks good to me |
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
LGTM. This closes a real gap: --kani-args (e.g. --include-pattern / --exclude-pattern) were parsed into command_args but dropped on the two autoharness --list branches, so --run list --with-autoharness and --run metrics --with-autoharness always processed the full function set.
The fix is consistent with how command_args is already forwarded to the verify-std autoharness (run-kani.sh:235/326), the autoharness run command (:361), and the analyzer command — this just brings the two --list branches into line.
No-op for existing CI: the "Kani List" / "Kani Metrics" jobs invoke these without --kani-args, so command_args is empty and "${command_args[@]}" expands to nothing. CI is green. Approving.
|
@tautschnig do you agree to merge this? |
5 participants
Summary
Forward arguments supplied through
--kani-argsto the AutoHarness listinvocations used by:
--run list --with-autoharness--run metrics --with-autoharnessMotivation
run-kani.shparses and stores arguments following--kani-args, but theAutoHarness list branches did not pass those arguments to Kani.
As a result, options such as
--include-patternand--exclude-patternweresilently ignored, causing
listandmetricsto process the completeAutoHarness function set instead of the requested subset.